In this section, we first formalize the semantic test
simplification problem, then prove its NP-Hardness.

%We then propose a heuristic algorithm that transforms a failed
%test into an easier-to-understand simplified test.


\subsection{Background Definitions}

{\textsc{\textbf{Definition 1.}}} {\it A unit test $t$ consists of
a sequence of statements $\overline{s}$ = \{$s_1$, $s_2$, ...,
$s_n$\} and a predicate $\phi$ as a testing oracle.}\vspace{1mm}

We write $t$ $\rightarrow$ $\phi$ when the execution of
$\overline{s}$ satisfies $\phi$. Similarly, we write $t$
$\nrightarrow$ $\phi$ when the execution of $\overline{s}$ does
\textit{not} satisfy $\phi$.  For example,\todo{This is not an example of
  $\nrightarrow$, which is the concept you just introduced in the previous
  sentence.  You should not change the subject after ``For example'', or at
  least should clarify what the example is of (what the new topic is).} the defect-revealing property $\phi$
of the failing test in Figure~\ref{fig:failedtest} is: \CodeIn{var9.equals(var9)}
returns \CodeIn{false} at line 10.

We use $|t|$ to denote the length of
a unit test $t$, which is equal to the number of statements in
$\overline{s}$. For instance, the length of \CodeIn{test1} in
Figure~\ref{fig:failedtest} is 9, and the length of
the simplified \CodeIn{test1} in Figure~\ref{fig:simplified} is 4.



\vspace{2mm}

{\textsc{\textbf{Definition 2.}}} {\it A statement $s$ $\in$
$\overline{s}$ in a unit test $t$ is either a \textit{value
declaration} statement or a \textit{method invocation} statement:
}\vspace{-7mm}

\todo{I don't like the ``value declaration'' terminology for what is just a
  variable assignment.  A method call creates a value too, so the term
  ``value declaration'' does not clarify what is different about the
  variable-to-variable assignment.}

\begin{align*}
s ::= {} &\ \ v_{out} \;\texttt{=}\; v_{in} \\
    & |\ v_{out} \;\texttt{=}\; \textit{m}(v_{in_1}, ..., v_{in_n}) \\
\end{align*}

\vspace{-5mm}

A value declaration statement simply assigns a value $v_{in}$ to
a declared variable $v_{out}$, and a method invocation statement
invokes method $m$ with argument variables $v_{in_1}$, $v_{in_2}$, ..., $v_{in_n}$ and
assigns the result to an output variable $v_{out}$. In our definition, method
invocation statements also include constructor calls and array declarations. We use
$\perp$ to denote $v_{out}$ if no output is available, such as
invoking a \CodeIn{void} method. For $s \in \overline{s}$,

\begin{align*}
\text{isValDecl}(s) &=
\left\{
    \begin{array}{ll}
        \text{T} & \text{s is a value declaration statement}\\
        \text{F} & \text{s is a method invocation statement}
    \end{array}
\right.
\end{align*}

and

\vspace{-5mm}

\begin{align*}
\text{isMethCall}(s) = \neg \; \text{isValDecl}(s) \quad\quad\quad\quad\quad\quad\quad\quad\quad\quad\quad\quad\quad
\end{align*}

\vspace{1mm}


For $s \in \overline{s}$, we use $\mathcal{O}(s)$ to denote its return
variable $v_{out}$, and use $\mathcal{I}(s)$ to denote its input
variable set:

\vspace{1mm}

\noindent
\begin{align*}
\mathcal{O}(s) = \left\{
\begin{array}{ll}
\perp & \mathrm{if}\mbox{ \text{isMethCall}(s) and \textit{returnType}(m)=\CodeIn{void}}\\
v_{out} & \mbox{ otherwise}\\
\end{array}\right.
\end{align*}



\vspace{1mm}

\noindent
\begin{align*}
\mathcal{I}(s) = \left\{
\begin{array}{ll}
\{ v_{in} \} & \mathrm{if}\mbox{ \text{isValDecl}(s)}\\
\{ v_{in_1},...,v_{in_n} \} & \mathrm{if}\mbox{ \text{isMethCall}(s)} \quad \quad \quad \quad \quad \quad \\
\end{array}\right.
\end{align*}

\vspace{1mm}

%We also use $\mathcal{I}(s)[k]$ to denote the $k$-th
%input variable $v_{in_k}$ of statement $s$.

For property $\phi$, $\mathcal{I}(\phi)$ denotes the
 input variables to evaluate $\phi$. To be a valid test, for each $v_i \in$ $\mathcal{I}(\phi)$, there must $\exists s \in \overline{s}$ that
$v_{i} = \mathcal{O}(s)$. $\mathcal{O}(\phi)$ denotes its evaluation result as:

\noindent
\begin{align*}
\mathcal{O}(\phi) = \left\{
\begin{array}{l l}
  \text{T} & \; \mbox{if $t$ $\rightarrow$ $\phi$} \;\quad \quad\quad \quad\quad \quad\quad \quad\quad \quad\quad \quad\quad \quad\quad\\
  \text{F} & \; \mbox{if $t$ $\nrightarrow$ $\phi$}\\ \end{array} \right.
\end{align*}



%For each variable $v_\alpha$, we use $\tau_\alpha$ to denote its
%static type.

\vspace{1mm}

For each $s \in \overline{s}$, we define:

\todo{``getValue'' is a weird name, if this is something that returns
  $\perp$ for method calls.  Method calls do produce a value.  So, rename
  ``getValue'' if you are going to keep its semantics the same.}


%\noindent \[\mathsf{getValue}(s) = \left\{
%\begin{array}{ll}
%v_{in} & \mathrm{if}\mbox{$\mathsf{isValDecl}$(s)}\\
%\perp & \mathrm{if}\mbox{ otherwise}\\
%\end{array}\right./]

\noindent
\begin{align*}
\text{getValue}(s) = \left\{
\begin{array}{ll}
 v_{in} & \mathrm{if}\mbox{ \text{isValDecl}(s)}\\
\perp & \mbox{ otherwise}\\
\end{array}\right.
\end{align*}

\vspace{1mm}

\noindent
\begin{align*}
\text{getMethod}(s) = \left\{
\begin{array}{ll}
 m & \mathrm{if}\mbox{ \text{isMethCall}(s)}\;\;\quad\\
\perp & \mbox{ otherwise}\\
\end{array}\right.
\end{align*}


\vspace{1mm}

For statements $s, s' \in \overline{s}$, we define:

\noindent $\text{SameStatementKind}$(s, s') =
\vspace{-2mm}
\begin{align*}
\left\{
\begin{array}{l l l}
  \text{T} & \; \mbox{if \; \text{isValDecl}(s) == \text{isValDecl}(s')}\quad\quad\\
   & \; \quad \quad \texttt{\&\&}\mbox{ \text{isMethCall}(s) == \text{isMethCall}(s')}\quad\;\\
  \text{F} & \; \mbox{otherwise}\\ \end{array} \right.
  \end{align*}

  \vspace{1mm}

\noindent $\text{SameValueOrMethod}$(s, s') =
\vspace{-2mm}
\begin{align*}
\left\{
\begin{array}{l l l l}
  \text{T} & \;\;\ \mbox{if \; \text{SameStatementKind}(s, s')}\\
   & \; \quad \quad \texttt{\&\&}\mbox{  \text{getValue}(s) == \text{getValue}(s')}\\
   & \; \quad \quad \texttt{\&\&}\mbox{ \text{getMethod}(s) == \text{getMethod}(s')}\\
  \text{F} & \; \mbox{otherwise}\\ \end{array} \right.
  \end{align*}

\todo{I don't understand the point of ``SameValueOrMethod''.  It would help
  to describe the specifcation or intended use of these functions, not just
  define them without comment.  In particulary, it's surprising to me
  (maybe because I don't understand the point of this) that the method
  arguments can differ but this function would still return true.}

\vspace{1mm}

%We finally define $SameValueOrMethod(s, s')$ as:

%\textit{(1) true, iff $SameStatement(s, s')$ and  $getValue(s)$ == $getValue(s')$
%and $getMethod(s)$ == $getMethod(s')$}
%\textit{(2) false, otherwise}
%\vspace{2mm}

{\textsc{\textbf{Definition 3.}}} {\it A unit test $t$ = $\overline{s}$ $\cup$ $\phi$ is
valid iff:}

\textit{(1) $\forall$ $s_i$ $\in$ $\overline{s}$, and $\forall$
$v$ $\in$ $\mathcal{I}(s_i)$, $\exists$ $s_j$ $\in$
$\overline{s}$ with $j$ $<$ $i$, such that $v$ = $\mathcal{O}(s_j)$.}\vspace{2mm}

\textit{(2) each statement $s$ $\in$ $\overline{s}$ is type-correct}

{\textsc{\textbf{Definition 4.}}} {\it Given a valid unit
test $t$ = $\overline{s}$ $\cup$ $\phi$ and $t$ $\rightarrow$
$\phi$, then $t'$ = $\overline{s'}$ $\cup$ $\phi$ is a simplified test of $t$
if $t'$ satisfies: }\vspace{1mm}

\textit{(1) $t'$ is valid} and $t'$ $\rightarrow$ $\phi$

\textit{(2) $\forall$ $s'_i$ $\in$
$\overline{s'}$}, \textit{$\exists$
$s$ $\in$ $\overline{s}$, $\text{SameValueOrMethod}(s'_i, s)$}



\textit{(3) $\forall$ $s'_i, s'_j \in \overline{s'}$ with
$i$ $<$ $j$, $\exists$ $s_k, s_p$ $\in$ $\overline{s}$ with 
$k$ $<$ $p$ and both $\text{SameValueOrMethod}(s'_i, s_k)$ and 
$\text{SameValueOrMethod}(s'_j, s_p)$ return true}.


\vspace{2mm}



\subsection{Problem Definition}

%As described earlier, we are given a test $t$ = $s_1$$s_2$...$s_n$
%that satisfied the bug predicate $\phi$ at the end of the
%execution. We want to find a simplified test $t_{min}$  such that
%$cost(t_{min})$ is the minimum of the cost of all valid test
%variants of $t$. Formally, let $T_{min}$ = \{$t'$ $|$ $t'$ is a
%valid test variant of $t$ and for all valid test variants $t''$,
%$cost(t')$ $\leq$ $cost(t'')$\}. The goal of our algorithm is to
%return an element of $T_{min}$.

We next formally define the \textit{semantic test simplification} problem.

{\textsc{\textbf{Definition 5.}}} {\it Given a valid test $t$
= $\overline{s}$ $\cup$ $\phi$ and $t$ $\rightarrow$ $\phi$, find a simplified
test $t_{min}$, such that: for any $t'$ that is also a simplified test of $t$, and $|t'|$ $\geq$ $|t_{min}|$ }.

\vspace{2mm}

The goal is to find a simplified test $t_{min}$  that has the shortest length
among all simplified tests and still satisfies $\phi$.
Such a test minimizes the number
of statements, which, in our view, is simpler than the
original test.

\vspace{1mm}

Unfortunately, the problem of finding an element of $t_{min}$ is
NP-hard. We next prove this claim by reducing the Set Cover
problem~\cite{kleinberg2006algorithm} to the test simplification problem.

%\proclaim{Theorem 1}

\vspace{2mm}

{\textsc{\textbf{Theorem 1}}}. {\it The problem of finding an
element of $t_{min}$ is NP-hard.}\vspace{1mm}

%$\spadesuit$ \textbf{The proof below is incorrect, I should use set cover problem}

\vspace{1mm}\noindent{\bf Proof. } (Sketch) In the Set Cover problem, we
are given a set of elements $U$ = \{$c_1$, ..., $c_m$\} (called the universe), and $n$
sets $S_1$, ..., $S_n$ whose union comprises the universe. The goal is to identify
the \textit{smallest} number of sets from $S_1$, ..., $S_n$ whose union still contains all elements in
the universe. The Set Cover problem is well known to be NP-hard~\cite{kleinberg2006algorithm}.

We now reduce the Set Cover problem to the semantic test simplification
problem. Assume we are given an arbitrary universe $U$ = \{$c_1$, ..., $c_m$\}
and $n$ sets $S_1$, ..., $S_n$ on which we must find the minimum
number of sets whose union comprises the universe $U$. We now
construct a test $t$ = $\overline{s}$ $\cup$ $\phi$ as follows:


\begin{itemize}

\item $\overline{s}$ consists of $n + m$ statements. The first $n$
statements are value declaration statements, and the next $m$
statements are non-\CodeIn{void} method invocation statements. For convenience, we
denote $n$ value declaration statements as: $s_{v_{1}}$, ..., $s_{v_{n}}$,
and denote $m$ method invocation statements as: $s_{c_1}$, ..., $s_{c_m}$.

\item Each of the $m$ method invocation statements takes exactly one
input variable, and returns one output variable. That is,
$|\mathcal{I}(s_{c_i})|$ = $|\mathcal{O}(s_{c_i})|$ = 1. For each
set $S_{i}$, if element $c_j$ $\in$ $S_{i}$, we denote the output
variable of statement $s_{v_{i}}$ can be used as the
input variable of statement $s_{c_j}$.

\item Predicate $\phi$ uses \textit{all} output variables of the $m$ method
invocation statements. That is, $|\mathcal{I}(\phi)|$ = $m$, and
for each $s_{c_i}$ with 1 $\leq$ $i$ $\leq$ $m$, $\mathcal{O}(s_{c_i})$ $\in$ $\mathcal{I}(\phi)$.
%$\forall$ $s$ $\in$ $\overline{s}$, $\mathcal{O}(s)$ $\in$ $\mathcal{I}(\phi)$ iff
%$isMethod(s)$.

%\item For each 1 $\leq$ $i$ $\leq$ $n$, 1 $\leq$ $j$ $\leq$ $m$, if
%$x_i$ $\in$ $C_j$, then $\mathcal{O}(s_{c_i})$ $\in$ $\mathcal{I}(s_{c_j})$.

\end{itemize}

In the above construction, $m$ method invocation statements can
not be removed, since $\phi$ uses all their output variables. Therefore,
in any simplified test $t'$ = $\overline{s'}$ $\cup$ $\phi$, 
$s_{c_i}$ $\in$ $\overline{s'}$ (1 $\leq$ i $\leq$ $m$).


Let $t_{min}$ = $\overline{s_{min}}$ $\cup$ $\phi$ be a minimally simplified
test. For each 1 $\leq$ i $\leq$ $n$, if $s_{v_i}$ $\in$ $\overline{s_{min}}$,
we add set $S_i$ to the result.  Since the size of $t_{min}$ has been minimized,
this leads to a minimal number of sets in the result. This shows that the test simplification problem is
NP-hard. $\Box$

%(Sketch) In the MinSAT problem, we are given a set of boolean variables
% $U$ = \{$x_1$, ..., $x_n$\} and a
%collection $C$ = \{$C_1$, ..., $C_m$\} of clauses over $U$. Each clause $C_i$ is of the
%form $z_1$$\vee$ $z_2$ $\vee$ ... $z_{k_i}$ ($k_i$ $\geq$ 1),
%where each $z_j$ is either a variable $x_l$ or its negation
%$\neg$$x_l$ The goal is to assign the variable $x_1$, ..., $x_n$
%boolean values 0 or 1 so that the total number of the satisfied
%clauses is minimized. The MinSAT problem is well known to be
%NP-hard~\cite{minsat}.


%simplification problem ($S$, $\preceq$, $\phi$) as follows. Let
%define a type set $\mathcal{T}$ = \{$t_1$, $t_2$, ..., $t_n$\}
%$\cup$ \{$\tau_1$\, $\tau_2$, ... $\tau_m$\}, each of the types
%corresponds to a boolean variable $x_i$. We use $t(x_i)$ to denote
%the corresponding type of $x_i$: $t_i$ $\in$ $\mathcal{T}$. We
%define $S$ = \{$s_i$ $|$ 0 $\leq$ $i$ $<$ $n$, $s_i$ is a
%declaration statement with $\mathcal{I}$($s_i$) = $\emptyset$ and
%$\mathcal{O_{s_i}}$= $t(x_i)$\} $\cup$ \{$s_i$ $|$ $n$ $\leq$ $i$
%$<$ $m$ + $n$, $s_i$ is a method call statement with
%$\mathcal{I}$($s_i$) = \{$t(x_i)$ $|$ $x_i$ $\in$ $C_{i-n}$\} and
%$\mathcal{O}$($s_i$) = $\tau_{i-n}$\}. $\preceq$ $=$ $\preceq_{t}$
%$\cup$ $\preceq_{p}$. $\phi$ is an assertion statement, for which
%$\mathcal{I}$($\phi$) = \{$\tau_1$, ..., $\tau_m$\} and
%$\mathcal{O}$($\phi$) = $\bot$.

%Let $t'$ = $\langle$$S'$, $\preceq'$, $\phi$$\rangle$ $\in$
%$T_{min}$. Assign $x_i$ be 1 if $x_i$ is not in $S'$, and all
%remaining $x_i$ be 0. This leads to a minimal number satisfied
%clauses. This shows that the test simplification problem is
%NP-hard. $\Box$

%\endproclaim


%(Sketch) Given a test $t$,
%consider a triple $\langle$$S$, $\preceq$, $\phi$$\rangle$, where
%$S$ is a set of statements and $\preceq$ is a partial-order
%relation on $S$. We require that $\preceq$ minimally relates all
%pairs of statements $s_i$, $s_j$ $\in$ $A$ $\cup$ $\phi$.
%\textit{Program-order} and \textit{type-compatible} relations are
%included in $\preceq$. The statements in a simplified test must
%conform to $\preceq$. Then, the test simplification problem
%becomes to come up with a new triple $\langle$$S'$, $\preceq'$,
%$\phi$$\rangle$, where $S'$ $\subset$ $S$ and $\preceq'$ $\subset$
%$\preceq$. Note that the relation between $S'$ and $\phi$ is also
%included in $\preceq'$.




%We now reduce the MinSAT problem to the semantic test simplification
%problem. We assume we are given an arbitrary set of boolean
%variables $U$ = \{$x_1$, $x_2$, ..., $x_n$\} and a collection of
%clauses $C$ = \{$C_1$, $C_2$, ..., $C_m$\} on which we must find
%the minimum set of satisfied clauses. We now construct a test
%$t$ = $\overline{s}$ $\cup$ $\phi$ as follows:



%Consider a failed unit test $t$. Let $S(t)$ = \{$s_1$, $s_2$, ...,
%$s_n$\} be the set of statements that are in $t$. For statement
%$s_i$ $\in$ $S(t)$, $s_i$ is either a value declaration statement,
%or a method-call statement (including method invocation,
%constructor call, and array creation). We denote each $s_i$ by a
%pair $\langle$$\mathcal{I}$$($$s_i$$)$,
%$\mathcal{O}_{s_i}$$\rangle$, where $\mathcal{I}$$($$s_i$$)$ is
%the list of input types of $s_i$, and $\mathcal{O}_{s_i}$ is the
%return type of $s_i$. We use $\mathcal{I}$$($$s_i$$)$[$k$] to
%denote the type of the $k^{th}$ input of $s_i$. Note that for a
%value declaration statement or an empty array declaration
%statement, $\mathcal{I}$$($$s_i$$)$ $=$ $\emptyset$.

%For statement $s_i$ $\in$ $S(t)$, we also define
%$\mathcal{IS}$$($$s_i$$)$ to denote a list of statements whose
%output values are used as the input values of $s_i$, and use
%$\mathcal{OV}$($s_i$ ) to denote the output value of $s_i$. To be
%a type-correct program, $|$$\mathcal{IS}$$($$s_i$$)$$|$ $=$
%$|$$\mathcal{I}$$($$s_i$$)$$|$, and $\mathcal{O}_{s_{k}}$
%$\sqsubseteq$ $\mathcal{I}$$($$s_i$$)$$[k]$, where $s_k$ $=$
%$\mathcal{IS}$$($$s_i$$)$$[k]$.

%We say the test fails if at the end of the execution the program
%state satisfies a predicate, say $\phi$, that denotes an assertion
%statement. For $\phi$, we use $\mathcal{I}$($\phi$) to denote its
%input types, and use $\mathcal{O_\phi}$ $=$ $\perp$ to denote
%there is no output value from an assertion statement. For the rest
%of this discussion, assume test $t$ fails by satisfying $\phi$ at
%the end of its execution. The goal of test simplification is to
%compute a \textit{simplified} but \textit{type-valid} test
%$t_{min}$ such that the state of the program after executing
%$t_{min}$ satisfies $\phi$. We next define the notation of test
%simplification formally.

%We say that two statements $s_i$ and $s_j$ are related by the
%\textit{program-order} relation, denoted by $s_i$ $\prec_t$ $s_j$,
%iff $i$ $<$ $j$. Such relation must be preserved after test
%simplification. We also define a \textit{type-compatible} relation
%$\prec_{t_{ijk}}$ between $s_i$ and $s_j$, denoted by $s_i$
%$\prec_{t_{ijk}}$ $s_j$ iff $\mathcal{O}_{s_{k}}$ $\leq$
%$\mathcal{I}$$($$s_i$$)$$[k]$, where $s_k$ $=$
%$\mathcal{IS}$$($$s_i$$)$$[k]$.

%Let's call a test $t'$ = $s_1'$$s_2'$...$s_k'$ a valid simplified
%test of $t$ if the following conditions hold:

%\begin{itemize}

%\item For any statement $s_i'$ $\in$ $S(t')$, $s_i'$ $\in$ $S(t)$

%\item For any two statements $s_i'$, $s_j'$ $\in$ $S(t')$, if
%$s_i'$ $\prec_{t'}$ $s_j'$, then $s_i'$ $\prec_{t}$ $s_j'$

%\item For statements $s_i'$, $s_j'$ $\in$ $S(t')$, for $0$ $\leq$
%$|$$\mathcal{I}$$($$s_j'$$)$$|$, $\mathcal{O}_{s_{k}'}$
%$\sqsubseteq$ $\mathcal{I}$$($$s_i'$$)$$[k]$, where $s_k$ $=$
%$\mathcal{IS}$$($$s_i'$$)$$[k]$.

%\end{itemize}

%We can associate a \textit{cost} function with a simplified test
%--- the cost of a simplified test $cost(t)$ is equal to
%$|$$S(t)$$|$, that is, the number of statements in $t$.
